/*
	Definitions for program inputs
*/

#define N 4
#define READERS 2


/*
	Macros for the writer
*/
inline inc_locally() {
		
	byte cb = N;
	wlc[cb] = (wlc[cb] + 1) % 2;
	wlc[2*N - 1 -cb] = wlc[cb];
	
	do
		:: (wlc[cb] == 0);
			if
				:: ((cb + 1) < 2*N);
					cb++;
					wlc[cb] = (wlc[cb] + 1) % 2;
					wlc[2*N - 1 -cb] = wlc[cb];
				:: ((cb + 1) >= 2*N);
					break;
			fi
		:: (wlc[cb] != 0);
			break;
	od;
	
}

inline sc_to_int(num) {
	d_step {
		num = 0;
		int i;
		for(i : 0 .. N-1) {
			num = num * 2;
			num = num + sc[i];
		}
	}
}

inline atomic_read(common, temp) {
	d_step {temp = common}
}